Report for code.c (Counterexample 3)

Generated on 2025-05-12 21:23:19 by CPAchecker 4.0 / default

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
#include <stdlib.h>  
2
#include <stdio.h>  
3
#include <assert.h>  
4
  
5
#define LEN 10  
6
  
7
extern unsigned __VERIFIER_nondet_uint();  
8
extern void __VERIFIER_assume(int);  
9
  
10
/* EXPLANATION  
11
 * The bug in this code is on line 20,the while loop  
12
 * The line needs to be (low <= high), so that the middle value isn't   
13
 * skipped when low and high converge  
14
 */  
15
  
16
// Preconditions:   
17
// arr is a sorted array  
18
// size is the size of the array arr   
19
int binary_search_function(int arr[], int size, int target) {  
20
    int low = 0;  
21
    int high = size - 1;  
22
    int mid;  
23
    while (low < high) {  
24
        mid = (low + high)/2;  
25
        if (arr[mid] == target) {  
26
            return mid;  
27
        }  
28
        if (arr[mid] < target) {  
29
            low = mid + 1;  
30
        }  
31
        if (arr[mid] > target) {  
32
            high = mid - 1;  
33
        }  
34
    }  
35
    return -1;  
36
}  
37
  
38
int dumb_sort(int arr[], int len, int target) {  
39
	for (int i=0; i<len; ++i) {  
40
		if (target == arr[i]) {  
41
			return i;  
42
		}  
43
	}  
44
  
45
	return -1;  
46
}  
47
  
48
int main() {  
49
  int arr[LEN] = {   
50
		__VERIFIER_nondet_int(),   
51
		__VERIFIER_nondet_int(),  
52
		__VERIFIER_nondet_int(),  
53
		__VERIFIER_nondet_int(),  
54
    __VERIFIER_nondet_int(),  
55
    __VERIFIER_nondet_int(),  
56
    __VERIFIER_nondet_int(),  
57
    __VERIFIER_nondet_int(),  
58
    __VERIFIER_nondet_int(),  
59
    __VERIFIER_nondet_int(),  
60
  };  
61
  
62
  int x = __VERIFIER_nondet_int();  
63
  
64
	for (int i=0; i<LEN-1; ++i) {  
65
		__VERIFIER_assume(arr[i] < arr[i+1]);  
66
	}  
67
  
68
  int result = binary_search_function(arr, LEN, x);  
69
  printf("Result of binary search is = %d\n", result);  
70
  
71
  // is the result correct? How can you check?  
72
	if (result != dumb_sort(arr, LEN, x)) {  
73
		assert(0);  
74
	}  
75
  
76
  return 1;  
77
}  
1
#include <stdlib.h>  
2
#include <stdio.h>  
3
#include <assert.h>  
4
  
5
#define LEN 10  
6
  
7
extern unsigned __VERIFIER_nondet_uint();  
8
extern void __VERIFIER_assume(int);  
9
  
10
/* EXPLANATION  
11
 * The bug in this code is on line 20,the while loop  
12
 * The line needs to be (low <= high), so that the middle value isn't   
13
 * skipped when low and high converge  
14
 */  
15
  
16
// Preconditions:   
17
// arr is a sorted array  
18
// size is the size of the array arr   
19
int binary_search_function(int arr[], int size, int target) {  
20
    int low = 0;  
21
    int high = size - 1;  
22
    int mid;  
23
    while (low < high) {  
24
        mid = (low + high)/2;  
25
        if (arr[mid] == target) {  
26
            return mid;  
27
        }  
28
        if (arr[mid] < target) {  
29
            low = mid + 1;  
30
        }  
31
        if (arr[mid] > target) {  
32
            high = mid - 1;  
33
        }  
34
    }  
35
    return -1;  
36
}  
37
  
38
int dumb_sort(int arr[], int len, int target) {  
39
	for (int i=0; i<len; ++i) {  
40
		if (target == arr[i]) {  
41
			return i;  
42
		}  
43
	}  
44
  
45
	return -1;  
46
}  
47
  
48
int main() {  
49
  int arr[LEN] = {   
50
		__VERIFIER_nondet_int(),   
51
		__VERIFIER_nondet_int(),  
52
		__VERIFIER_nondet_int(),  
53
		__VERIFIER_nondet_int(),  
54
    __VERIFIER_nondet_int(),  
55
    __VERIFIER_nondet_int(),  
56
    __VERIFIER_nondet_int(),  
57
    __VERIFIER_nondet_int(),  
58
    __VERIFIER_nondet_int(),  
59
    __VERIFIER_nondet_int(),  
60
  };  
61
  
62
  int x = __VERIFIER_nondet_int();  
63
  
64
	for (int i=0; i<LEN-1; ++i) {  
65
		__VERIFIER_assume(arr[i] < arr[i+1]);  
66
	}  
67
  
68
  int result = binary_search_function(arr, LEN, x);  
69
  printf("Result of binary search is = %d\n", result);  
70
  
71
  // is the result correct? How can you check?  
72
	if (result != dumb_sort(arr, LEN, x)) {  
73
		assert(0);  
74
	}  
75
  
76
  return 1;  
77
}  
1
/* Macros and inline functions to swap the order of bytes in integer values.  
2
   Copyright (C) 1997-2020 Free Software Foundation, Inc.  
3
   This file is part of the GNU C Library.  
4
  
5
   The GNU C Library is free software; you can redistribute it and/or  
6
   modify it under the terms of the GNU Lesser General Public  
7
   License as published by the Free Software Foundation; either  
8
   version 2.1 of the License, or (at your option) any later version.  
9
  
10
   The GNU C Library is distributed in the hope that it will be useful,  
11
   but WITHOUT ANY WARRANTY; without even the implied warranty of  
12
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  
13
   Lesser General Public License for more details.  
14
  
15
   You should have received a copy of the GNU Lesser General Public  
16
   License along with the GNU C Library; if not, see  
17
   <https://www.gnu.org/licenses/>.  */  
18
  
19
#if !defined _BYTESWAP_H && !defined _NETINET_IN_H && !defined _ENDIAN_H  
20
# error "Never use <bits/byteswap.h> directly; include <byteswap.h> instead."  
21
#endif  
22
  
23
#ifndef _BITS_BYTESWAP_H  
24
#define _BITS_BYTESWAP_H 1  
25
  
26
#include <features.h>  
27
#include <bits/types.h>  
28
  
29
/* Swap bytes in 16-bit value.  */  
30
#define __bswap_constant_16(x)					\  
31
  ((__uint16_t) ((((x) >> 8) & 0xff) | (((x) & 0xff) << 8)))  
32
  
33
static __inline __uint16_t  
34
__bswap_16 (__uint16_t __bsx)  
35
{  
36
#if __GNUC_PREREQ (4, 8)  
37
  return __builtin_bswap16 (__bsx);  
38
#else  
39
  return __bswap_constant_16 (__bsx);  
40
#endif  
41
}  
42
  
43
/* Swap bytes in 32-bit value.  */  
44
#define __bswap_constant_32(x)					\  
45
  ((((x) & 0xff000000u) >> 24) | (((x) & 0x00ff0000u) >> 8)	\  
46
   | (((x) & 0x0000ff00u) << 8) | (((x) & 0x000000ffu) << 24))  
47
  
48
static __inline __uint32_t  
49
__bswap_32 (__uint32_t __bsx)  
50
{  
51
#if __GNUC_PREREQ (4, 3)  
52
  return __builtin_bswap32 (__bsx);  
53
#else  
54
  return __bswap_constant_32 (__bsx);  
55
#endif  
56
}  
57
  
58
/* Swap bytes in 64-bit value.  */  
59
#define __bswap_constant_64(x)			\  
60
  ((((x) & 0xff00000000000000ull) >> 56)	\  
61
   | (((x) & 0x00ff000000000000ull) >> 40)	\  
62
   | (((x) & 0x0000ff0000000000ull) >> 24)	\  
63
   | (((x) & 0x000000ff00000000ull) >> 8)	\  
64
   | (((x) & 0x00000000ff000000ull) << 8)	\  
65
   | (((x) & 0x0000000000ff0000ull) << 24)	\  
66
   | (((x) & 0x000000000000ff00ull) << 40)	\  
67
   | (((x) & 0x00000000000000ffull) << 56))  
68
  
69
__extension__ static __inline __uint64_t  
70
__bswap_64 (__uint64_t __bsx)  
71
{  
72
#if __GNUC_PREREQ (4, 3)  
73
  return __builtin_bswap64 (__bsx);  
74
#else  
75
  return __bswap_constant_64 (__bsx);  
76
#endif  
77
}  
78
  
79
#endif /* _BITS_BYTESWAP_H */  
1
/* Inline functions to return unsigned integer values unchanged.  
2
   Copyright (C) 2017-2020 Free Software Foundation, Inc.  
3
   This file is part of the GNU C Library.  
4
  
5
   The GNU C Library is free software; you can redistribute it and/or  
6
   modify it under the terms of the GNU Lesser General Public  
7
   License as published by the Free Software Foundation; either  
8
   version 2.1 of the License, or (at your option) any later version.  
9
  
10
   The GNU C Library is distributed in the hope that it will be useful,  
11
   but WITHOUT ANY WARRANTY; without even the implied warranty of  
12
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  
13
   Lesser General Public License for more details.  
14
  
15
   You should have received a copy of the GNU Lesser General Public  
16
   License along with the GNU C Library; if not, see  
17
   <https://www.gnu.org/licenses/>.  */  
18
  
19
#if !defined _NETINET_IN_H && !defined _ENDIAN_H  
20
# error "Never use <bits/uintn-identity.h> directly; include <netinet/in.h> or <endian.h> instead."  
21
#endif  
22
  
23
#ifndef _BITS_UINTN_IDENTITY_H  
24
#define _BITS_UINTN_IDENTITY_H 1  
25
  
26
#include <bits/types.h>  
27
  
28
/* These inline functions are to ensure the appropriate type  
29
   conversions and associated diagnostics from macros that convert to  
30
   a given endianness.  */  
31
  
32
static __inline __uint16_t  
33
__uint16_identity (__uint16_t __x)  
34
{  
35
  return __x;  
36
}  
37
  
38
static __inline __uint32_t  
39
__uint32_identity (__uint32_t __x)  
40
{  
41
  return __x;  
42
}  
43
  
44
static __inline __uint64_t  
45
__uint64_identity (__uint64_t __x)  
46
{  
47
  return __x;  
48
}  
49
  
50
#endif /* _BITS_UINTN_IDENTITY_H.  */  
DateTimeLevelComponentMessage
2025-05-1221:22:58:956INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-05-1221:22:59:040INFOCPAchecker.runCPAchecker 4.0 / default (OpenJDK 64-Bit Server VM 17.0.14) started
2025-05-1221:22:59:064INFOCPAchecker.parseParsing CFA from file(s) "code.c"
2025-05-1221:23:00:441WARNINGCheckBindingVisitor.visitUndefined function __VERIFIER_nondet_int found, first called in line 50
2025-05-1221:23:01:711INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2025-05-1221:23:01:728WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.callstack.unsupportedFunctions
2025-05-1221:23:01:729INFOCPAchecker.runAlgorithmStarting analysis ...
2025-05-1221:23:01:740INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2025-05-1221:23:01:748INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
CoreComponentsFactory.createAlgorithm
Using Restarting Algorithm
2025-05-1221:23:01:761INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.run
Loading analysis 1 from file /cpachecker/config/components/parallel-valueAnalysis.properties ...
2025-05-1221:23:01:780INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
ResourceLimitChecker.fromConfiguration
Using the following resource limits: Thread CPU-time limit of 90s
2025-05-1221:23:02:258INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:23:02:493INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
InductionStepCase
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:23:02:530INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.run
Starting analysis 1 ...
2025-05-1221:23:02:912INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:03:317INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheckAlgorithm.checkCounterexample
Error path found, starting counterexample check with CPACHECKER.
2025-05-1221:23:03:725WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int();
2025-05-1221:23:03:825WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int();
2025-05-1221:23:03:838WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int();
2025-05-1221:23:03:854WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int();
2025-05-1221:23:03:869WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int();
2025-05-1221:23:03:880WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int();
2025-05-1221:23:03:883WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int();
2025-05-1221:23:03:885WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int();
2025-05-1221:23:03:894WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int();
2025-05-1221:23:03:922WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int();
2025-05-1221:23:04:056WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int();
2025-05-1221:23:04:233INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:04:297INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:04:664INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheckAlgorithm.checkCounterexample
Error path found, starting counterexample check with CPACHECKER.
2025-05-1221:23:05:581INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:05:812WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
AutomatonGraphmlParser.getSpecAsProperties
Cannot map specification // This file is part of CPAchecker,
// a tool for configurable software verification:
// https://cpachecker.sosy-lab.org
//
// SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0
OBSERVER AUTOMATON AssertionAutomaton
// This automaton detects assertions that may fail
// (i.e., a function call to __assert_fail).
INITIAL STATE Init;
STATE USEFIRST Init :
// Match standard calls to __assert_fail with nice message on violations.
MATCH {__assert_fail($1, $2, $3, $4)}
-> ERROR("assertion in $location: Condition $1 failed in $2, line $3");
// Match if assert_fail or assert_func is called with any number of parameters.
MATCH {__assert_fail($?)} || MATCH {__assert_func($?)}
-> ERROR("assertion in $location");
// Print warnings for other common error functions to warn users about potentially wrong specification.
MATCH {assert($?)} && !CHECK(location, "functionName==assert")
-> PRINT "WARNING: Function assert() without body detected. Please run the C preprocessor on this file to enable assertion checking."
GOTO Init;
MATCH {__VERIFIER_error($?)} && !CHECK(location, "functionName==__VERIFIER_error")
-> PRINT "WARNING: Function __VERIFIER_error() is ignored by this specification. If you want to check for reachability of __VERIFIER_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
MATCH {reach_error($?)}
-> PRINT "WARNING: Function reach_error() is ignored by this specification. If you want to check for reachability of reach_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
END AUTOMATON to property type. Will ignore it (would only be problematic if this were the termination property).
2025-05-1221:23:05:983WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
AutomatonGraphmlParser.getSpecAsProperties
Cannot map specification // This file is part of CPAchecker,
// a tool for configurable software verification:
// https://cpachecker.sosy-lab.org
//
// SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0
OBSERVER AUTOMATON AssertionAutomaton
// This automaton detects assertions that may fail
// (i.e., a function call to __assert_fail).
INITIAL STATE Init;
STATE USEFIRST Init :
// Match standard calls to __assert_fail with nice message on violations.
MATCH {__assert_fail($1, $2, $3, $4)}
-> ERROR("assertion in $location: Condition $1 failed in $2, line $3");
// Match if assert_fail or assert_func is called with any number of parameters.
MATCH {__assert_fail($?)} || MATCH {__assert_func($?)}
-> ERROR("assertion in $location");
// Print warnings for other common error functions to warn users about potentially wrong specification.
MATCH {assert($?)} && !CHECK(location, "functionName==assert")
-> PRINT "WARNING: Function assert() without body detected. Please run the C preprocessor on this file to enable assertion checking."
GOTO Init;
MATCH {__VERIFIER_error($?)} && !CHECK(location, "functionName==__VERIFIER_error")
-> PRINT "WARNING: Function __VERIFIER_error() is ignored by this specification. If you want to check for reachability of __VERIFIER_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
MATCH {reach_error($?)}
-> PRINT "WARNING: Function reach_error() is ignored by this specification. If you want to check for reachability of reach_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
END AUTOMATON to property type. Will ignore it (would only be problematic if this were the termination property).
2025-05-1221:23:06:344INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:23:06:345INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:23:06:353WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
Repository.addMBean
Warning: Error during registration of management interface AbstractionPredicatesMBean (org.sosy_lab.cpachecker:type=predicate,name=AbstractionPredicates)
2025-05-1221:23:06:548WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int();
2025-05-1221:23:06:555WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int();
2025-05-1221:23:06:562WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int();
2025-05-1221:23:06:568WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int();
2025-05-1221:23:06:573WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int();
2025-05-1221:23:06:578WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int();
2025-05-1221:23:06:581WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int();
2025-05-1221:23:06:585WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int();
2025-05-1221:23:06:587WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int();
2025-05-1221:23:06:588WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int();
2025-05-1221:23:06:591WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int();
2025-05-1221:23:06:600WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int();
2025-05-1221:23:06:604WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int();
2025-05-1221:23:06:604WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int();
2025-05-1221:23:06:608WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int();
2025-05-1221:23:06:616WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int();
2025-05-1221:23:06:616WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int();
2025-05-1221:23:06:626WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int();
2025-05-1221:23:06:630WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int();
2025-05-1221:23:06:647WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int();
2025-05-1221:23:06:665WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int();
2025-05-1221:23:06:665WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int();
2025-05-1221:23:06:944INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:07:053INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheckAlgorithm.checkCounterexample
Error path found but identified as infeasible.
2025-05-1221:23:07:054INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheckAlgorithm.checkCounterexample
Error path found but identified as infeasible.
2025-05-1221:23:07:094INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 2
2025-05-1221:23:07:095INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:07:108INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:07:111INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:07:189INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:07:612INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:07:764INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 3
2025-05-1221:23:07:764INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:07:769INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:07:770INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:07:842INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:08:281INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:08:445INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 4
2025-05-1221:23:08:446INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:08:451INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:08:452INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:08:510INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:08:888INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:09:152INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 5
2025-05-1221:23:09:152INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:09:169INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:09:170INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:09:207INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:09:842INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:10:161INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 6
2025-05-1221:23:10:162INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:10:165INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:10:166INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:10:209INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:10:816INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:11:158INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 7
2025-05-1221:23:11:159INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:11:164INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:11:165INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:11:286INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:12:014INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:12:670INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 8
2025-05-1221:23:12:671INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:12:674INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:12:675INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:12:728INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:13:405INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:13:882INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 9
2025-05-1221:23:13:883INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:13:885INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:13:886INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:23:13:923INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:23:14:847INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:23:15:746INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 10
2025-05-1221:23:15:746INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:23:15:855INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:23:16:317INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.analyzeCounterexample0
Error found, creating error path
2025-05-1221:23:16:512INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
ParallelAlgorithm.handleFutureResults
/cpachecker/config/components/parallel-kInduction.properties finished successfully.
2025-05-1221:23:16:515INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.skipNextAnalysesIfRequired
Ignoring restart configuration '/cpachecker/config/components/recursion.properties' because condition if-recursive did not match.
2025-05-1221:23:16:516INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.skipNextAnalysesIfRequired
Ignoring restart configuration '/cpachecker/config/components/concurrency.properties' because condition if-concurrent did not match.
2025-05-1221:23:16:517INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set 0
Used algorithm property /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Program containing only relevant bools 0
Relevant boolean vars / relevant vars ratio 0.3704
Requires alias handling 0
Requires loop handling 1
Has a single loop 0
Requires composite-type handling 0
Requires array handling 1
Requires float handling 0
Requires recursion handling 0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions true
Number of all righthand side functions 3
Restart Algorithm statistics
Number of algorithms provided 3
Number of algorithms used 3
Last algorithm used /cpachecker/config/components/concurrency.properties
Total time for algorithm 3 14.757s
Parallel Algorithm statistics
Number of algorithms used 3
Successful analysis /cpachecker/config/components/parallel-kInduction.properties
Statistics for /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties
=======================================================================================
Time spent in analysis thread /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties 0.002s
ValueAnalysisCPA statistics
Number of variables per state 2.56 sum: 407, count: 159, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 159, min: 0, max: 0
Number of assumptions 84
Number of deterministic assumptions 38
Level of Determinism 45%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 159
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.026s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.056s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 551, count: 551, min: 1, max: 1 [1 x 551]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 145
Max size of waitlist 14
Average size of waitlist 4
Number of computed successors 159
Max successors for one state 2
Number of times merged 0
Number of times stopped 1
Number of times breaked 1
Total time for CPA algorithm 0.768s Max: 0.768s
Time for choose from waitlist 0.000s
Time for precision adjustment 0.075s
Time for transfer relation 0.588s
Time for stop operator 0.084s
Time for adding to reached set 0.010s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 3.741s
Statistics for /cpachecker/config/components/parallel-valueAnalysis-itp-end.properties
=======================================================================================
ValueAnalysisCPA statistics
Number of variables per state 1.58 sum: 220, count: 139, min: 0, max: 4
Number of global variables per state 0.00 sum: 0, count: 139, min: 0, max: 0
Number of assumptions 212
Number of deterministic assumptions 50
Level of Determinism 24%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 478
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.039s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.119s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2034, count: 2034, min: 1, max: 1 [1 x 2034]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 417
Max size of waitlist 9
Average size of waitlist 2
Number of computed successors 478
Max successors for one state 2
Number of times merged 0
Number of times stopped 50
Number of times breaked 4
Total time for CPA algorithm 0.821s Max: 0.407s
Time for choose from waitlist 0.007s
Time for precision adjustment 0.076s
Time for transfer relation 0.644s
Time for stop operator 0.058s
Time for adding to reached set 0.009s
ValueAnalysisRefiner statistics
Number of refinements 4
Number of targets found 4 count: 4, min: 1, max: 1, avg: 1.00
Time for completing refinement 0.936s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 3
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.068s
Number of interpolations 3
Number of interpolation queries 11 count: 133, min: 0, max: 3, avg: 0.08
Size of interpolant 0.08 sum: 10, count: 133, min: 0, max: 2
Number of sliced prefixes 7 count: 3, min: 1, max: 4, avg: 2.33
Extracting infeasible sliced prefixes 0.274s
Selecting infeasible sliced prefixes 0.029s
CEGAR algorithm statistics
Number of CEGAR refinements 4
Number of successful refinements 3
Number of failed refinements 0
Max. size of reached set before ref. 139
Max. size of reached set after ref. 1
Avg. size of reached set before ref. 108.00
Avg. size of reached set after ref. 1.00
Total time for CEGAR algorithm 2.116s
Time for refinements 1.294s
Average time for refinement 0.323s
Max time for refinement 0.525s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 2.396s
Statistics for /cpachecker/config/components/parallel-kInduction.properties
============================================================================
PredicateCPA statistics
Number of abstractions 99 5% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 0 0%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 99 100%
Times precision was empty 99 100%
Times precision was {false} 0 0%
Times result was cached 0 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 0 0%
Times result was 'false' 0 0%
Number of strengthen sat checks 0
Number of coverage checks 58
BDD entailment checks 0
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 161
Avg ABE block size 116.34 sum: 11518, count: 99, min: 72, max: 161
Number of predicates discovered 0
Time for post operator 0.522s
Time for path formula creation 0.504s
Time for strengthen operator 0.055s
Time for prec operator 0.030s
Time for abstraction 0.000s Max: 0.000s, Count: 99
Solving time 0.000s Max: 0.000s
Model enumeration time 0.000s
Time for BDD construction 0.000s Max: 0.000s
Time for merge operator 0.004s
Time for coverage checks 0.000s
Total time for SMT solver (w/o itp) 0.000s
Total number of created targets for pointer analysis 0
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
Bounds CPA statistics
Bound k 10
Maximum loop iteration reached 11
ValueAnalysisCPA statistics
Number of variables per state 1.87 sum: 3632, count: 1939, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 1939, min: 0, max: 0
Number of assumptions 718
Number of deterministic assumptions 242
Level of Determinism 34%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 1976
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.010s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.012s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 1976, count: 1976, min: 1, max: 1 [1 x 1976]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 1957
Max size of waitlist 190
Average size of waitlist 74
LoopstackSortedWaitlist 2.72 sum: 1431, count: 526, min: 0, max: 707
ReversePostorderSortedWaitlist 1.69 sum: 905, count: 537, min: 0, max: 698
LoopIterationSortedWaitlist 2.70 sum: 1420, count: 526, min: 0, max: 707
CallstackSortedWaitlist 152.10 sum: 1521, count: 10, min: 2, max: 1431
Number of computed successors 1976
Max successors for one state 2
Number of times merged 29
Number of times stopped 29
Number of times breaked 0
Total time for CPA algorithm 1.451s Max: 1.302s
Time for choose from waitlist 0.097s
Time for precision adjustment 0.230s
Time for transfer relation 0.972s
Time for merge operator 0.011s
Time for stop operator 0.024s
Time for adding to reached set 0.064s
BMC algorithm statistics
Time for BMC formula creation 1.467s
Time for final sat check 0.503s
Time for error-path creation 0.031s
Time for error-path post-processing 0.139s
Time for bounding assertions check 0.376s
Time for induction formula creation 6.115s
Time for induction check 3.389s
Other statistics
================
Parallel Algorithm statistics
Number of algorithms used 3
Successful analysis /cpachecker/config/components/parallel-kInduction.properties
Statistics for /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties
=======================================================================================
Time spent in analysis thread /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties 0.002s
ValueAnalysisCPA statistics
Number of variables per state 2.56 sum: 407, count: 159, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 159, min: 0, max: 0
Number of assumptions 84
Number of deterministic assumptions 38
Level of Determinism 45%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 159
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.026s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.056s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 551, count: 551, min: 1, max: 1 [1 x 551]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 145
Max size of waitlist 14
Average size of waitlist 4
Number of computed successors 159
Max successors for one state 2
Number of times merged 0
Number of times stopped 1
Number of times breaked 1
Total time for CPA algorithm 0.768s Max: 0.768s
Time for choose from waitlist 0.000s
Time for precision adjustment 0.075s
Time for transfer relation 0.588s
Time for stop operator 0.084s
Time for adding to reached set 0.010s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 3.741s
Statistics for /cpachecker/config/components/parallel-valueAnalysis-itp-end.properties
=======================================================================================
ValueAnalysisCPA statistics
Number of variables per state 1.58 sum: 220, count: 139, min: 0, max: 4
Number of global variables per state 0.00 sum: 0, count: 139, min: 0, max: 0
Number of assumptions 212
Number of deterministic assumptions 50
Level of Determinism 24%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 478
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.039s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.119s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2034, count: 2034, min: 1, max: 1 [1 x 2034]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 417
Max size of waitlist 9
Average size of waitlist 2
Number of computed successors 478
Max successors for one state 2
Number of times merged 0
Number of times stopped 50
Number of times breaked 4
Total time for CPA algorithm 0.821s Max: 0.407s
Time for choose from waitlist 0.007s
Time for precision adjustment 0.076s
Time for transfer relation 0.644s
Time for stop operator 0.058s
Time for adding to reached set 0.009s
ValueAnalysisRefiner statistics
Number of refinements 4
Number of targets found 4 count: 4, min: 1, max: 1, avg: 1.00
Time for completing refinement 0.936s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 3
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.068s
Number of interpolations 3
Number of interpolation queries 11 count: 133, min: 0, max: 3, avg: 0.08
Size of interpolant 0.08 sum: 10, count: 133, min: 0, max: 2
Number of sliced prefixes 7 count: 3, min: 1, max: 4, avg: 2.33
Extracting infeasible sliced prefixes 0.274s
Selecting infeasible sliced prefixes 0.029s
CEGAR algorithm statistics
Number of CEGAR refinements 4
Number of successful refinements 3
Number of failed refinements 0
Max. size of reached set before ref. 139
Max. size of reached set after ref. 1
Avg. size of reached set before ref. 108.00
Avg. size of reached set after ref. 1.00
Total time for CEGAR algorithm 2.116s
Time for refinements 1.294s
Average time for refinement 0.323s
Max time for refinement 0.525s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 2.396s
Statistics for /cpachecker/config/components/parallel-kInduction.properties
============================================================================
PredicateCPA statistics
Number of abstractions 99 5% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 0 0%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 99 100%
Times precision was empty 99 100%
Times precision was {false} 0 0%
Times result was cached 0 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 0 0%
Times result was 'false' 0 0%
Number of strengthen sat checks 0
Number of coverage checks 58
BDD entailment checks 0
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 161
Avg ABE block size 116.34 sum: 11518, count: 99, min: 72, max: 161
Number of predicates discovered 0
Time for post operator 0.522s
Time for path formula creation 0.504s
Time for strengthen operator 0.055s
Time for prec operator 0.030s
Time for abstraction 0.000s Max: 0.000s, Count: 99
Solving time 0.000s Max: 0.000s
Model enumeration time 0.000s
Time for BDD construction 0.000s Max: 0.000s
Time for merge operator 0.004s
Time for coverage checks 0.000s
Total time for SMT solver (w/o itp) 0.000s
Total number of created targets for pointer analysis 0
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
Bounds CPA statistics
Bound k 10
Maximum loop iteration reached 11
ValueAnalysisCPA statistics
Number of variables per state 1.87 sum: 3632, count: 1939, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 1939, min: 0, max: 0
Number of assumptions 718
Number of deterministic assumptions 242
Level of Determinism 34%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 1976
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.010s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.012s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 1976, count: 1976, min: 1, max: 1 [1 x 1976]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 1957
Max size of waitlist 190
Average size of waitlist 74
LoopstackSortedWaitlist 2.72 sum: 1431, count: 526, min: 0, max: 707
ReversePostorderSortedWaitlist 1.69 sum: 905, count: 537, min: 0, max: 698
LoopIterationSortedWaitlist 2.70 sum: 1420, count: 526, min: 0, max: 707
CallstackSortedWaitlist 152.10 sum: 1521, count: 10, min: 2, max: 1431
Number of computed successors 1976
Max successors for one state 2
Number of times merged 29
Number of times stopped 29
Number of times breaked 0
Total time for CPA algorithm 1.451s Max: 1.302s
Time for choose from waitlist 0.097s
Time for precision adjustment 0.230s
Time for transfer relation 0.972s
Time for merge operator 0.011s
Time for stop operator 0.024s
Time for adding to reached set 0.064s
BMC algorithm statistics
Time for BMC formula creation 1.467s
Time for final sat check 0.503s
Time for error-path creation 0.031s
Time for error-path post-processing 0.139s
Time for bounding assertions check 0.376s
Time for induction formula creation 6.115s
Time for induction check 3.389s
Other statistics
================
Code Coverage
Function coverage 0.333
Visited lines 465
Total lines 472
Line coverage 0.985
Visited conditions 17
Total conditions 18
Condition coverage 0.944
CPAchecker general statistics
Number of program locations 478
Number of CFA edges (per node) 477 count: 478, min: 0, max: 2, avg: 1.00
Number of relevant variables 27
Number of functions 9
Number of loops (and loop nodes) 3 sum: 18, min: 4, max: 10, avg: 6.00
Size of reached set 1939
Number of reached locations 452 95%
Avg states per location 4
Max states per location 110 at node N54
Number of reached functions 3 33%
Number of target states 99
Time for analysis setup 2.664s
Time for loading CPAs 0.948s
Time for loading parser 0.317s
Time for CFA construction 1.363s
Time for parsing file(s) 0.450s
Time for AST to CFA 0.466s
Time for CFA sanity check 0.036s
Time for post-processing 0.215s
Time for loop structure 0.009s
Time for AST structure 0.000s
Time for CFA export 0.774s
Time for function pointers resolving 0.004s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.120s
Time for collecting variables 0.077s
Time for solving dependencies 0.004s
Time for building hierarchy 0.000s
Time for building classification 0.034s
Time for exporting data 0.005s
Time for Analysis 14.784s
CPU time for analysis 26.080s
Time for analyzing result 0.003s
Total time for CPAchecker 17.457s
Total CPU time for CPAchecker 31.280s
Time for statistics 0.172s
Time for Garbage Collector 0.247s in 50 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 99MB ( 94 MiB) max; 48MB ( 46 MiB) avg; 113MB ( 108 MiB) peak
Used non-heap memory 67MB ( 64 MiB) max; 55MB ( 53 MiB) avg; 68MB ( 65 MiB) peak
Used in PS Old Gen pool 70MB ( 67 MiB) max; 28MB ( 27 MiB) avg; 70MB ( 67 MiB) peak
Allocated heap memory 132MB ( 126 MiB) max; 126MB ( 120 MiB) avg
Allocated non-heap memory 70MB ( 66 MiB) max; 58MB ( 55 MiB) avg
Total process virtual memory 5521MB ( 5266 MiB) max; 5358MB ( 5110 MiB) avg
#Configuration NameConfiguration Value
1analysis.name default
2analysis.programNames code.c
3analysis.selectAnalysisHeuristically true
4cfa.useCFACloningForMultiThreadedPrograms true
5cpa.callstack.unsupportedFunctions pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp,atexit
6datarace.config dataRaceAnalysis.properties
7heuristicSelection.addressedRatio 0.0
8heuristicSelection.complexLoopConfig components/configselection-restart-valueAnalysis-fallbacks.properties
9heuristicSelection.loopConfig components/multipleLoopsConfig.properties
10heuristicSelection.loopFreeConfig components/configselection-restart-bmc-fallbacks.properties
11heuristicSelection.singleLoopConfig components/singleLoopConfig.properties
12language C
13log.level INFO
14memorycleanup.config smg-memorycleanup.properties
15memorysafety.config smg-memorysafety.properties
16overflow.config overflowAnalysis.properties
17parser.usePreprocessor true
18specification /cpachecker/config/specification/Assertion.spc
19termination.config terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}